T:Type, f:(TT).
retraction(T;f)  (y, x:T. y is f*(x)  f(x) is f*(y)  ((y = x)  (y = f(x)))) 

latex

Definitions	t  T, x:AB(x), Type, retraction(T;f), s = t, , a < b, x:A  B(x), x:A. B(x), x:A. B(x), A, f(a), <a, b>, , y is f*(x), Void, P  Q, False, left + right, P  Q, hd(l), y=f*(x) via L, Dec(P), P & Q, P  Q, , A  B, Atom, {i..j}, b, x,y:A//B(x;y), b | a, a ~ b, |p|, a  b, a <p b, |g|, a < b, A c B, x f y, |r|, xL. P(x), (xL.P(x)), Unit, , , type List, (x  l), x.A(x), {T}, x,y. t(x;y), s ~ t, SQType(T)
Lemmas	retraction-fun-path, guard wf, fun-connected-step, decidable wf, false wf, fun-connected transitivity, retraction wf, fun-connected-induction, fun-connected wf, not wf